A,B:es_realizer{i:l}.
R-Feasible{i:l}
R-Feasible(A)
 R-Feasible{i:l}
 R-Feasible(B)
 (i:Id
 (((j:Id. R-has-loc(A; j) = eq_id(i; j)  )
 ( fpf-all(Knd;
 ( fpf-all(Kind-deq;
 ( fpf-all(R-da(A; i);
 ( fpf-all(k,T.((isrcv(k))
 ( fpf-all( (((source(lnk(k)) = i  Id)
 ( fpf-all(  subtype_rel(T; fpf-cap(R-da(B; destination(lnk(k))); Kind-deq; k; top)))
 ( fpf-all(  ((destination(lnk(k)) = i  Id)
 ( fpf-all(   subtype_rel(fpf-cap(R-da(B; source(lnk(k))); Kind-deq; k; void); T)))))))
 R-icompat(A; B) 

latex

Definitions	guard(T), sq_type(T), True, T, prop{i:l}, P  Q, P  Q, x. t(x), t  T, fpf-all(A; eq; f; x,v.P(x;v)), P  Q, x:A. B(x), P  Q, x:A. B(x), x(s)
Lemmas	R-interface-iff2, Id sq, assert-eq-id, true wf, squash wf, R-interface-iff, es realizer wf, R-Feasible wf, ldst wf, fpf-cap wf, fpf-ap wf, lnk wf, lsrc wf, isrcv wf, top wf, fpf wf, fpf-trivial-subtype-top, R-da wf, Kind-deq wf, fpf-dom wf, assert wf, Knd wf, eq id wf, R-has-loc wf, bool wf, Id wf, R-interface-icompat